Private Specification, Partial Struct Encoding, and Constructor #619

vizual1 · 2023-02-08T18:31:06Z

Added the pvt() function into Gobra that takes an expression and gives a boolean to indicate if it is private within the package (it does not get imported from other packages). Currently, it is used inside the type checker. Additionally, it can be used inside specifications:

requires pvt(E)
preserves pvt(E)
ensures pvt(E)
func foo(E typ)

assert pvt(foo)

are all valid expressions right now. There may be some bugs for pure functions and predicates because they are imported into other packages with the body.

Added private specifications for functions and methods. To ensure soundness, a private proof statement is added into the private specification. It is written as:

requires P
ensures Q
private {
  requires p
  ensures q
  proof foo {
    R = foo(A)
  }
}
func foo(A) R

Changed how the private fields of structs get encoded (on import), by removing the private fields and changing it into a partial_struct. For example, if we have a struct with private field c and import it into another package:

type S struct { 
  Left, Right, c int 
}

then it would be changed into

type bar.S partial_struct {
  Left, Right int
}

In the viper encoding a partial_struct removes an axiom from the Tuple Domain to disallow the comparison of two partial_structs.

func foo(x, y bar.S) {
  if (x.Left == y.Left && x.Right = y.Right) {
    assert x == y //fail
  }
}

In viper that means:

// if we removed the private field without changing the encoding (struct)
domain Tuple2[A, B] {
  function get0(t: Tuple2[A, B]): A
  function get1(t: Tuple2[A, B]): B
  function create2(a: A, b: B): Tuple2[A, B]

  axiom {
    forall t: Tuple2[A, B] :: {get0(t)} {get1(t)} t == create2(get0(t), get1(t))
  }

  axiom {
    forall a: A, b: B :: {create2(a,b)} get0(create2(a,b)) == a && get1(create2(a,b)) == b
  }
}

get changed to:

// if we removed the private field and change the encoding (partial_struct)
domain Tuple2[A, B] {
  function get0(t: Tuple2[A, B]): A
  function get1(t: Tuple2[A, B]): B
  function create2(a: A, b: B): Tuple2[A, B]

  axiom {
    forall a: A, b: B :: {create2(a,b)} get0(create2(a,b)) == a && get1(create2(a,b)) == b
  }
}

Please check the written code and if additional documentations are needed in some places. (Also there might be some small bits of a constructor, which is not finished yet.)

Felalolf

First batch of comments.

src/main/antlr4/.antlr/GoLexer.java

src/main/antlr4/GobraLexer.g4

src/main/antlr4/GobraParser.g4

src/main/scala/viper/gobra/ast/internal/Program.scala

src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala

src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala

src/main/scala/viper/gobra/translator/util/TypePatterns.scala

vizual1 · 2023-02-28T15:30:23Z

Added a construct, dereference, and assignment declaration to be able to define and abstract permission for structs.

type T struct { F, g int }

pred (t *T) Mem() { acc(&t.g) }

ensures acc(&this.F) && this.Mem()
construct &T() {
  fold this.Mem()
}

requires acc(&this.F) && this.Mem()
pure deref &T() {
  return unfolding this.Mem() in *this
}

requires acc(&this.F) && this.Mem()
ensures acc(&this.F) && this.Mem()
ensures *this == rhs //deref(this)
assign &T(rhs T) {
  unfold this.Mem()
  *this = rhs
  fold this.Mem()
}

The specifications need to be public.

Felalolf

More comments. I have not yet looked at the desugarer, the ConstructorEncoding, the AssignmentEncoding, and the DerefEncoding

src/main/scala/viper/gobra/ast/frontend/Ast.scala

src/main/scala/viper/gobra/ast/internal/Program.scala

src/main/scala/viper/gobra/frontend/info/ExternalTypeInfo.scala

src/main/scala/viper/gobra/translator/encodings/structs/StructEncoding.scala

Felalolf · 2023-03-06T15:16:19Z

src/main/scala/viper/gobra/translator/encodings/structs/StructEncoding.scala

+    case (loc: in.Location) :: ctx.CompleteStruct(_) / Shared =>
+      val deref = ctx.lookupDereference(loc.typ)
+      if (deref.isEmpty) { sh.convertToExclusive(loc)(ctx, ex) }
+      else { 
+        val (pos, info, errT) = loc.vprMeta
+        val funcName = deref.getOrElse(null).uniqueName
+        for {
+          b <- bind(loc)(ctx)
+          v = variable(ctx)(b).localVar
+          func = vpr.FuncApp(funcName, Seq(v))(pos, info, v.typ, errT)
+        } yield func
+      }
+
+    case (loc: in.Location) :: ctx.PartialStruct(_) / Shared =>
+      val deref = ctx.lookupDereference(loc.typ)
+      if (deref.isEmpty) { sh.convertToExclusive(loc)(ctx, pex) }
+      else { 
+        val (pos, info, errT) = loc.vprMeta
+        val funcName = deref.getOrElse(null).uniqueName
+        for {
+          b <- bind(loc)(ctx)
+          v = variable(ctx)(b).localVar
+          func = vpr.FuncApp(funcName, Seq(v))(pos, info, v.typ, errT)
+        } yield func
+      }


I would have expected that for CompleteStruct it is always sh.convertToExclusive(...) and for PartialStruct, it is always the call to the deref function (there is an error if there is no deref function).

If we always use sh.convertToExclusive(...) for a CompleteStruct, then this statement would fail:

requires acc(&a.Left) && acc(&a.Right) && a.PrivateMem() func foo(a *Pair) { x := *a // fails, not enough permission }

Since there is no call to dereference, Pair that has fields Left, Right, p does not have access to the field p (within the same package until we unfold a.PrivateMem()). The constructor always gets called once defined, therefore:

x := &Pair{Left: 2, Right: 0, p: 1} assert(x.PrivateMem()) //constructor ensures x.PrivateMem()

and the assignment y := *x would fail, despite constructing x just before.

The question is if we want to explicitly unfold x.PrivateMem() or just let the dereference handle it.

src/main/scala/viper/gobra/translator/encodings/structs/AssignmentsEncoding.scala

src/main/scala/viper/gobra/translator/encodings/structs/DereferenceEncoding.scala

Felalolf

More comments. I have not yet looked at the desugarer, the ConstructorEncoding, the AssignmentEncoding, and the DerefEncoding

tho added 4 commits February 4, 2023 19:12

Visibility

9b424d9

Visibility

243e8b5

visibility

df1cc65

Visibility

84d0ff8

vizual1 marked this pull request as draft February 8, 2023 18:32

vizual1 marked this pull request as ready for review February 9, 2023 15:51

vizual1 marked this pull request as draft February 9, 2023 15:52

Felalolf reviewed Feb 15, 2023

View reviewed changes

Added constructor, dereference, and assignment

1953827

vizual1 changed the title ~~Private Specification and Partial Struct Encoding~~ Private Specification, Partial Struct Encoding, and Constructor Feb 28, 2023

jcp19 mentioned this pull request Mar 5, 2023

Dataplane viperproject/VerifiedSCION#169

Closed

20 tasks

Felalolf reviewed Mar 6, 2023

View reviewed changes

tho added 9 commits March 12, 2023 18:49

Updated Constructors, TypeChecking, Errors

408a4b7

Fixing some bugs-

d900138

git submodule updated

b7a6ca3

Fixed some of the comments, and bug fixes

d175042

Changed error messages, bug fixes

686bd12

Bug fixes, tests, added more errors and type check

9d8f337

some changes, bugfixes, evaluation tests

0ba28fd

bugfixes + documentation

f713622

Cleaned code up, documentations

891a4c3

Felalolf marked this pull request as ready for review May 17, 2023 17:34

Felalolf marked this pull request as draft May 17, 2023 17:37

jcp19 mentioned this pull request Jul 12, 2023

Problems with selective importing #166

Open

jcp19 mentioned this pull request Apr 29, 2024

Add opaque modifier viperproject/gobra-libs#12

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Private Specification, Partial Struct Encoding, and Constructor #619

Private Specification, Partial Struct Encoding, and Constructor #619

vizual1 commented Feb 8, 2023

Felalolf left a comment

vizual1 commented Feb 28, 2023

Felalolf left a comment

Felalolf Mar 6, 2023

vizual1 Mar 16, 2023 •

edited

Loading

Felalolf left a comment

Private Specification, Partial Struct Encoding, and Constructor #619

Are you sure you want to change the base?

Private Specification, Partial Struct Encoding, and Constructor #619

Conversation

vizual1 commented Feb 8, 2023

Felalolf left a comment

Choose a reason for hiding this comment

vizual1 commented Feb 28, 2023

Felalolf left a comment

Choose a reason for hiding this comment

Felalolf Mar 6, 2023

Choose a reason for hiding this comment

vizual1 Mar 16, 2023 • edited Loading

Choose a reason for hiding this comment

Felalolf left a comment

Choose a reason for hiding this comment

vizual1 Mar 16, 2023 •

edited

Loading